Nuprl Definition : sorted-by
11,40
postcript
pdf
sorted-by(
R
;
L
) ==
i
:{0..||
L
||
},
j
:{0..
i
}.
R
(
L
[
j
],
L
[
i
])
latex
Definitions
||
as
||
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
#$n
,
f
(
a
)
,
l
[
i
]
FDL editor aliases
sorted-by
origin
i:{0..||L||
}, j:{0..i}. R(L[j],L[i]) i:{0..||L||}, j:{0..i}. R(L[j],L[i]) x:A. B(x)}